(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(s(x1)) → s(s(s(p(s(b(p(p(s(s(x1))))))))))
b(s(x1)) → s(s(s(p(p(s(s(c(p(s(p(s(x1))))))))))))
c(s(x1)) → p(s(p(s(a(p(s(p(s(x1)))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
A(s(z0)) → c1(P(s(b(p(p(s(s(z0))))))), B(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
B(s(z0)) → c2(P(p(s(s(c(p(s(p(s(z0))))))))), P(s(s(c(p(s(p(s(z0)))))))), C(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
C(s(z0)) → c3(P(s(p(s(a(p(s(p(s(z0))))))))), P(s(a(p(s(p(s(z0))))))), A(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
P(p(s(z0))) → c4(P(z0))
S tuples:
A(s(z0)) → c1(P(s(b(p(p(s(s(z0))))))), B(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
B(s(z0)) → c2(P(p(s(s(c(p(s(p(s(z0))))))))), P(s(s(c(p(s(p(s(z0)))))))), C(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
C(s(z0)) → c3(P(s(p(s(a(p(s(p(s(z0))))))))), P(s(a(p(s(p(s(z0))))))), A(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
P(p(s(z0))) → c4(P(z0))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
A, B, C, P
Compound Symbols:
c1, c2, c3, c4
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
P(p(s(z0))) → c4(P(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
A(s(z0)) → c1(P(s(b(p(p(s(s(z0))))))), B(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
B(s(z0)) → c2(P(p(s(s(c(p(s(p(s(z0))))))))), P(s(s(c(p(s(p(s(z0)))))))), C(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
C(s(z0)) → c3(P(s(p(s(a(p(s(p(s(z0))))))))), P(s(a(p(s(p(s(z0))))))), A(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
S tuples:
A(s(z0)) → c1(P(s(b(p(p(s(s(z0))))))), B(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
B(s(z0)) → c2(P(p(s(s(c(p(s(p(s(z0))))))))), P(s(s(c(p(s(p(s(z0)))))))), C(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
C(s(z0)) → c3(P(s(p(s(a(p(s(p(s(z0))))))))), P(s(a(p(s(p(s(z0))))))), A(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
A, B, C
Compound Symbols:
c1, c2, c3
(5) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 11 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
A(s(z0)) → c1(B(p(p(s(s(z0))))))
B(s(z0)) → c2(C(p(s(p(s(z0))))))
C(s(z0)) → c3(A(p(s(p(s(z0))))))
S tuples:
A(s(z0)) → c1(B(p(p(s(s(z0))))))
B(s(z0)) → c2(C(p(s(p(s(z0))))))
C(s(z0)) → c3(A(p(s(p(s(z0))))))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
A, B, C
Compound Symbols:
c1, c2, c3
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
s(
z0)) →
c1(
B(
p(
p(
s(
s(
z0)))))) by
A(s(x0)) → c1(B(p(s(x0))))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
B(s(z0)) → c2(C(p(s(p(s(z0))))))
C(s(z0)) → c3(A(p(s(p(s(z0))))))
A(s(x0)) → c1(B(p(s(x0))))
S tuples:
B(s(z0)) → c2(C(p(s(p(s(z0))))))
C(s(z0)) → c3(A(p(s(p(s(z0))))))
A(s(x0)) → c1(B(p(s(x0))))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
B, C, A
Compound Symbols:
c2, c3, c1
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
s(
z0)) →
c2(
C(
p(
s(
p(
s(
z0)))))) by
B(s(x0)) → c2(C(p(s(x0))))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
C(s(z0)) → c3(A(p(s(p(s(z0))))))
A(s(x0)) → c1(B(p(s(x0))))
B(s(x0)) → c2(C(p(s(x0))))
S tuples:
C(s(z0)) → c3(A(p(s(p(s(z0))))))
A(s(x0)) → c1(B(p(s(x0))))
B(s(x0)) → c2(C(p(s(x0))))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
C, A, B
Compound Symbols:
c3, c1, c2
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
C(
s(
z0)) →
c3(
A(
p(
s(
p(
s(
z0)))))) by
C(s(x0)) → c3(A(p(s(x0))))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
A(s(x0)) → c1(B(p(s(x0))))
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
S tuples:
A(s(x0)) → c1(B(p(s(x0))))
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
A, B, C
Compound Symbols:
c1, c2, c3
(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
s(
x0)) →
c1(
B(
p(
s(
x0)))) by
A(s(z0)) → c1(B(z0))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
A(s(z0)) → c1(B(z0))
S tuples:
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
A(s(z0)) → c1(B(z0))
K tuples:none
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
B, C, A
Compound Symbols:
c2, c3, c1
(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
C(s(x0)) → c3(A(p(s(x0))))
A(s(z0)) → c1(B(z0))
We considered the (Usable) Rules:
p(s(z0)) → z0
And the Tuples:
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
A(s(z0)) → c1(B(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(A(x1)) = [3] + [2]x1
POL(B(x1)) = [4] + [2]x1
POL(C(x1)) = [4] + [2]x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(p(x1)) = x1
POL(s(x1)) = [4] + x1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(s(z0)) → s(s(s(p(s(b(p(p(s(s(z0))))))))))
b(s(z0)) → s(s(s(p(p(s(s(c(p(s(p(s(z0))))))))))))
c(s(z0)) → p(s(p(s(a(p(s(p(s(z0)))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
Tuples:
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
A(s(z0)) → c1(B(z0))
S tuples:
B(s(x0)) → c2(C(p(s(x0))))
K tuples:
C(s(x0)) → c3(A(p(s(x0))))
A(s(z0)) → c1(B(z0))
Defined Rule Symbols:
a, b, c, p
Defined Pair Symbols:
B, C, A
Compound Symbols:
c2, c3, c1
(17) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
B(s(x0)) → c2(C(p(s(x0))))
C(s(x0)) → c3(A(p(s(x0))))
Now S is empty
(18) BOUNDS(O(1), O(1))